0 CpxTRS
↳1 TrsToWeightedTrsProof (BOTH BOUNDS(ID, ID), 0 ms)
↳2 CpxWeightedTrs
↳3 CpxWeightedTrsRenamingProof (BOTH BOUNDS(ID, ID), 0 ms)
↳4 CpxWeightedTrs
↳5 InnermostUnusableRulesProof (BOTH BOUNDS(ID, ID), 0 ms)
↳6 CpxWeightedTrs
↳7 TypeInferenceProof (BOTH BOUNDS(ID, ID), 0 ms)
↳8 CpxTypedWeightedTrs
↳9 CompletionProof (UPPER BOUND(ID), 0 ms)
↳10 CpxTypedWeightedCompleteTrs
↳11 CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID), 0 ms)
↳12 CpxRNTS
↳13 CompleteCoflocoProof (⇔, 20.2 s)
↳14 BOUNDS(1, n^3)
U11(tt, V1, V2) → U12(isNatKind(activate(V1)), activate(V1), activate(V2))
U12(tt, V1, V2) → U13(isNatKind(activate(V2)), activate(V1), activate(V2))
U13(tt, V1, V2) → U14(isNatKind(activate(V2)), activate(V1), activate(V2))
U14(tt, V1, V2) → U15(isNat(activate(V1)), activate(V2))
U15(tt, V2) → U16(isNat(activate(V2)))
U16(tt) → tt
U21(tt, V1) → U22(isNatKind(activate(V1)), activate(V1))
U22(tt, V1) → U23(isNat(activate(V1)))
U23(tt) → tt
U31(tt, V2) → U32(isNatKind(activate(V2)))
U32(tt) → tt
U41(tt) → tt
U51(tt, N) → U52(isNatKind(activate(N)), activate(N))
U52(tt, N) → activate(N)
U61(tt, M, N) → U62(isNatKind(activate(M)), activate(M), activate(N))
U62(tt, M, N) → U63(isNat(activate(N)), activate(M), activate(N))
U63(tt, M, N) → U64(isNatKind(activate(N)), activate(M), activate(N))
U64(tt, M, N) → s(plus(activate(N), activate(M)))
isNat(n__0) → tt
isNat(n__plus(V1, V2)) → U11(isNatKind(activate(V1)), activate(V1), activate(V2))
isNat(n__s(V1)) → U21(isNatKind(activate(V1)), activate(V1))
isNatKind(n__0) → tt
isNatKind(n__plus(V1, V2)) → U31(isNatKind(activate(V1)), activate(V2))
isNatKind(n__s(V1)) → U41(isNatKind(activate(V1)))
plus(N, 0) → U51(isNat(N), N)
plus(N, s(M)) → U61(isNat(M), M, N)
0 → n__0
plus(X1, X2) → n__plus(X1, X2)
s(X) → n__s(X)
activate(n__0) → 0
activate(n__plus(X1, X2)) → plus(activate(X1), activate(X2))
activate(n__s(X)) → s(activate(X))
activate(X) → X
U11(tt, V1, V2) → U12(isNatKind(activate(V1)), activate(V1), activate(V2)) [1]
U12(tt, V1, V2) → U13(isNatKind(activate(V2)), activate(V1), activate(V2)) [1]
U13(tt, V1, V2) → U14(isNatKind(activate(V2)), activate(V1), activate(V2)) [1]
U14(tt, V1, V2) → U15(isNat(activate(V1)), activate(V2)) [1]
U15(tt, V2) → U16(isNat(activate(V2))) [1]
U16(tt) → tt [1]
U21(tt, V1) → U22(isNatKind(activate(V1)), activate(V1)) [1]
U22(tt, V1) → U23(isNat(activate(V1))) [1]
U23(tt) → tt [1]
U31(tt, V2) → U32(isNatKind(activate(V2))) [1]
U32(tt) → tt [1]
U41(tt) → tt [1]
U51(tt, N) → U52(isNatKind(activate(N)), activate(N)) [1]
U52(tt, N) → activate(N) [1]
U61(tt, M, N) → U62(isNatKind(activate(M)), activate(M), activate(N)) [1]
U62(tt, M, N) → U63(isNat(activate(N)), activate(M), activate(N)) [1]
U63(tt, M, N) → U64(isNatKind(activate(N)), activate(M), activate(N)) [1]
U64(tt, M, N) → s(plus(activate(N), activate(M))) [1]
isNat(n__0) → tt [1]
isNat(n__plus(V1, V2)) → U11(isNatKind(activate(V1)), activate(V1), activate(V2)) [1]
isNat(n__s(V1)) → U21(isNatKind(activate(V1)), activate(V1)) [1]
isNatKind(n__0) → tt [1]
isNatKind(n__plus(V1, V2)) → U31(isNatKind(activate(V1)), activate(V2)) [1]
isNatKind(n__s(V1)) → U41(isNatKind(activate(V1))) [1]
plus(N, 0) → U51(isNat(N), N) [1]
plus(N, s(M)) → U61(isNat(M), M, N) [1]
0 → n__0 [1]
plus(X1, X2) → n__plus(X1, X2) [1]
s(X) → n__s(X) [1]
activate(n__0) → 0 [1]
activate(n__plus(X1, X2)) → plus(activate(X1), activate(X2)) [1]
activate(n__s(X)) → s(activate(X)) [1]
activate(X) → X [1]
| 0 => 0' |
U11(tt, V1, V2) → U12(isNatKind(activate(V1)), activate(V1), activate(V2)) [1]
U12(tt, V1, V2) → U13(isNatKind(activate(V2)), activate(V1), activate(V2)) [1]
U13(tt, V1, V2) → U14(isNatKind(activate(V2)), activate(V1), activate(V2)) [1]
U14(tt, V1, V2) → U15(isNat(activate(V1)), activate(V2)) [1]
U15(tt, V2) → U16(isNat(activate(V2))) [1]
U16(tt) → tt [1]
U21(tt, V1) → U22(isNatKind(activate(V1)), activate(V1)) [1]
U22(tt, V1) → U23(isNat(activate(V1))) [1]
U23(tt) → tt [1]
U31(tt, V2) → U32(isNatKind(activate(V2))) [1]
U32(tt) → tt [1]
U41(tt) → tt [1]
U51(tt, N) → U52(isNatKind(activate(N)), activate(N)) [1]
U52(tt, N) → activate(N) [1]
U61(tt, M, N) → U62(isNatKind(activate(M)), activate(M), activate(N)) [1]
U62(tt, M, N) → U63(isNat(activate(N)), activate(M), activate(N)) [1]
U63(tt, M, N) → U64(isNatKind(activate(N)), activate(M), activate(N)) [1]
U64(tt, M, N) → s(plus(activate(N), activate(M))) [1]
isNat(n__0) → tt [1]
isNat(n__plus(V1, V2)) → U11(isNatKind(activate(V1)), activate(V1), activate(V2)) [1]
isNat(n__s(V1)) → U21(isNatKind(activate(V1)), activate(V1)) [1]
isNatKind(n__0) → tt [1]
isNatKind(n__plus(V1, V2)) → U31(isNatKind(activate(V1)), activate(V2)) [1]
isNatKind(n__s(V1)) → U41(isNatKind(activate(V1))) [1]
plus(N, 0') → U51(isNat(N), N) [1]
plus(N, s(M)) → U61(isNat(M), M, N) [1]
0' → n__0 [1]
plus(X1, X2) → n__plus(X1, X2) [1]
s(X) → n__s(X) [1]
activate(n__0) → 0' [1]
activate(n__plus(X1, X2)) → plus(activate(X1), activate(X2)) [1]
activate(n__s(X)) → s(activate(X)) [1]
activate(X) → X [1]
plus(N, 0') → U51(isNat(N), N) [1]
plus(N, s(M)) → U61(isNat(M), M, N) [1]
0' → n__0 [1]
s(X) → n__s(X) [1]
U11(tt, V1, V2) → U12(isNatKind(activate(V1)), activate(V1), activate(V2)) [1]
U12(tt, V1, V2) → U13(isNatKind(activate(V2)), activate(V1), activate(V2)) [1]
U13(tt, V1, V2) → U14(isNatKind(activate(V2)), activate(V1), activate(V2)) [1]
U14(tt, V1, V2) → U15(isNat(activate(V1)), activate(V2)) [1]
U15(tt, V2) → U16(isNat(activate(V2))) [1]
U16(tt) → tt [1]
U21(tt, V1) → U22(isNatKind(activate(V1)), activate(V1)) [1]
U22(tt, V1) → U23(isNat(activate(V1))) [1]
U23(tt) → tt [1]
U31(tt, V2) → U32(isNatKind(activate(V2))) [1]
U32(tt) → tt [1]
U41(tt) → tt [1]
U51(tt, N) → U52(isNatKind(activate(N)), activate(N)) [1]
U52(tt, N) → activate(N) [1]
U61(tt, M, N) → U62(isNatKind(activate(M)), activate(M), activate(N)) [1]
U62(tt, M, N) → U63(isNat(activate(N)), activate(M), activate(N)) [1]
U63(tt, M, N) → U64(isNatKind(activate(N)), activate(M), activate(N)) [1]
U64(tt, M, N) → s(plus(activate(N), activate(M))) [1]
isNat(n__0) → tt [1]
isNat(n__plus(V1, V2)) → U11(isNatKind(activate(V1)), activate(V1), activate(V2)) [1]
isNat(n__s(V1)) → U21(isNatKind(activate(V1)), activate(V1)) [1]
isNatKind(n__0) → tt [1]
isNatKind(n__plus(V1, V2)) → U31(isNatKind(activate(V1)), activate(V2)) [1]
isNatKind(n__s(V1)) → U41(isNatKind(activate(V1))) [1]
0' → n__0 [1]
plus(X1, X2) → n__plus(X1, X2) [1]
s(X) → n__s(X) [1]
activate(n__0) → 0' [1]
activate(n__plus(X1, X2)) → plus(activate(X1), activate(X2)) [1]
activate(n__s(X)) → s(activate(X)) [1]
activate(X) → X [1]
U11(tt, V1, V2) → U12(isNatKind(activate(V1)), activate(V1), activate(V2)) [1]
U12(tt, V1, V2) → U13(isNatKind(activate(V2)), activate(V1), activate(V2)) [1]
U13(tt, V1, V2) → U14(isNatKind(activate(V2)), activate(V1), activate(V2)) [1]
U14(tt, V1, V2) → U15(isNat(activate(V1)), activate(V2)) [1]
U15(tt, V2) → U16(isNat(activate(V2))) [1]
U16(tt) → tt [1]
U21(tt, V1) → U22(isNatKind(activate(V1)), activate(V1)) [1]
U22(tt, V1) → U23(isNat(activate(V1))) [1]
U23(tt) → tt [1]
U31(tt, V2) → U32(isNatKind(activate(V2))) [1]
U32(tt) → tt [1]
U41(tt) → tt [1]
U51(tt, N) → U52(isNatKind(activate(N)), activate(N)) [1]
U52(tt, N) → activate(N) [1]
U61(tt, M, N) → U62(isNatKind(activate(M)), activate(M), activate(N)) [1]
U62(tt, M, N) → U63(isNat(activate(N)), activate(M), activate(N)) [1]
U63(tt, M, N) → U64(isNatKind(activate(N)), activate(M), activate(N)) [1]
U64(tt, M, N) → s(plus(activate(N), activate(M))) [1]
isNat(n__0) → tt [1]
isNat(n__plus(V1, V2)) → U11(isNatKind(activate(V1)), activate(V1), activate(V2)) [1]
isNat(n__s(V1)) → U21(isNatKind(activate(V1)), activate(V1)) [1]
isNatKind(n__0) → tt [1]
isNatKind(n__plus(V1, V2)) → U31(isNatKind(activate(V1)), activate(V2)) [1]
isNatKind(n__s(V1)) → U41(isNatKind(activate(V1))) [1]
0' → n__0 [1]
plus(X1, X2) → n__plus(X1, X2) [1]
s(X) → n__s(X) [1]
activate(n__0) → 0' [1]
activate(n__plus(X1, X2)) → plus(activate(X1), activate(X2)) [1]
activate(n__s(X)) → s(activate(X)) [1]
activate(X) → X [1]
| U11 :: tt → n__0:n__plus:n__s → n__0:n__plus:n__s → tt tt :: tt U12 :: tt → n__0:n__plus:n__s → n__0:n__plus:n__s → tt isNatKind :: n__0:n__plus:n__s → tt activate :: n__0:n__plus:n__s → n__0:n__plus:n__s U13 :: tt → n__0:n__plus:n__s → n__0:n__plus:n__s → tt U14 :: tt → n__0:n__plus:n__s → n__0:n__plus:n__s → tt U15 :: tt → n__0:n__plus:n__s → tt isNat :: n__0:n__plus:n__s → tt U16 :: tt → tt U21 :: tt → n__0:n__plus:n__s → tt U22 :: tt → n__0:n__plus:n__s → tt U23 :: tt → tt U31 :: tt → n__0:n__plus:n__s → tt U32 :: tt → tt U41 :: tt → tt U51 :: tt → n__0:n__plus:n__s → n__0:n__plus:n__s U52 :: tt → n__0:n__plus:n__s → n__0:n__plus:n__s U61 :: tt → n__0:n__plus:n__s → n__0:n__plus:n__s → n__0:n__plus:n__s U62 :: tt → n__0:n__plus:n__s → n__0:n__plus:n__s → n__0:n__plus:n__s U63 :: tt → n__0:n__plus:n__s → n__0:n__plus:n__s → n__0:n__plus:n__s U64 :: tt → n__0:n__plus:n__s → n__0:n__plus:n__s → n__0:n__plus:n__s s :: n__0:n__plus:n__s → n__0:n__plus:n__s plus :: n__0:n__plus:n__s → n__0:n__plus:n__s → n__0:n__plus:n__s n__0 :: n__0:n__plus:n__s n__plus :: n__0:n__plus:n__s → n__0:n__plus:n__s → n__0:n__plus:n__s n__s :: n__0:n__plus:n__s → n__0:n__plus:n__s 0' :: n__0:n__plus:n__s |
| Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules:
The TRS has the following type information:
Rewrite Strategy: INNERMOST |
tt => 0
n__0 => 0
0' -{ 1 }→ 0 :|:
U11(z, z', z'') -{ 1 }→ U12(isNatKind(activate(V1)), activate(V1), activate(V2)) :|: V1 >= 0, V2 >= 0, z = 0, z'' = V2, z' = V1
U12(z, z', z'') -{ 1 }→ U13(isNatKind(activate(V2)), activate(V1), activate(V2)) :|: V1 >= 0, V2 >= 0, z = 0, z'' = V2, z' = V1
U13(z, z', z'') -{ 1 }→ U14(isNatKind(activate(V2)), activate(V1), activate(V2)) :|: V1 >= 0, V2 >= 0, z = 0, z'' = V2, z' = V1
U14(z, z', z'') -{ 1 }→ U15(isNat(activate(V1)), activate(V2)) :|: V1 >= 0, V2 >= 0, z = 0, z'' = V2, z' = V1
U15(z, z') -{ 1 }→ U16(isNat(activate(V2))) :|: z' = V2, V2 >= 0, z = 0
U16(z) -{ 1 }→ 0 :|: z = 0
U21(z, z') -{ 1 }→ U22(isNatKind(activate(V1)), activate(V1)) :|: V1 >= 0, z = 0, z' = V1
U22(z, z') -{ 1 }→ U23(isNat(activate(V1))) :|: V1 >= 0, z = 0, z' = V1
U23(z) -{ 1 }→ 0 :|: z = 0
U31(z, z') -{ 1 }→ U32(isNatKind(activate(V2))) :|: z' = V2, V2 >= 0, z = 0
U32(z) -{ 1 }→ 0 :|: z = 0
U41(z) -{ 1 }→ 0 :|: z = 0
U51(z, z') -{ 1 }→ U52(isNatKind(activate(N)), activate(N)) :|: z' = N, z = 0, N >= 0
U52(z, z') -{ 1 }→ activate(N) :|: z' = N, z = 0, N >= 0
U61(z, z', z'') -{ 1 }→ U62(isNatKind(activate(M)), activate(M), activate(N)) :|: z' = M, z = 0, z'' = N, M >= 0, N >= 0
U62(z, z', z'') -{ 1 }→ U63(isNat(activate(N)), activate(M), activate(N)) :|: z' = M, z = 0, z'' = N, M >= 0, N >= 0
U63(z, z', z'') -{ 1 }→ U64(isNatKind(activate(N)), activate(M), activate(N)) :|: z' = M, z = 0, z'' = N, M >= 0, N >= 0
U64(z, z', z'') -{ 1 }→ s(plus(activate(N), activate(M))) :|: z' = M, z = 0, z'' = N, M >= 0, N >= 0
activate(z) -{ 1 }→ X :|: X >= 0, z = X
activate(z) -{ 1 }→ s(activate(X)) :|: z = 1 + X, X >= 0
activate(z) -{ 1 }→ plus(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 1 }→ 0' :|: z = 0
isNat(z) -{ 1 }→ U21(isNatKind(activate(V1)), activate(V1)) :|: z = 1 + V1, V1 >= 0
isNat(z) -{ 1 }→ U11(isNatKind(activate(V1)), activate(V1), activate(V2)) :|: V1 >= 0, V2 >= 0, z = 1 + V1 + V2
isNat(z) -{ 1 }→ 0 :|: z = 0
isNatKind(z) -{ 1 }→ U41(isNatKind(activate(V1))) :|: z = 1 + V1, V1 >= 0
isNatKind(z) -{ 1 }→ U31(isNatKind(activate(V1)), activate(V2)) :|: V1 >= 0, V2 >= 0, z = 1 + V1 + V2
isNatKind(z) -{ 1 }→ 0 :|: z = 0
plus(z, z') -{ 1 }→ 1 + X1 + X2 :|: X1 >= 0, X2 >= 0, z = X1, z' = X2
s(z) -{ 1 }→ 1 + X :|: X >= 0, z = X
| eq(start(V, V3, V4),0,[fun(V, V3, V4, Out)],[V >= 0,V3 >= 0,V4 >= 0]). eq(start(V, V3, V4),0,[fun1(V, V3, V4, Out)],[V >= 0,V3 >= 0,V4 >= 0]). eq(start(V, V3, V4),0,[fun2(V, V3, V4, Out)],[V >= 0,V3 >= 0,V4 >= 0]). eq(start(V, V3, V4),0,[fun3(V, V3, V4, Out)],[V >= 0,V3 >= 0,V4 >= 0]). eq(start(V, V3, V4),0,[fun4(V, V3, Out)],[V >= 0,V3 >= 0]). eq(start(V, V3, V4),0,[fun5(V, Out)],[V >= 0]). eq(start(V, V3, V4),0,[fun6(V, V3, Out)],[V >= 0,V3 >= 0]). eq(start(V, V3, V4),0,[fun7(V, V3, Out)],[V >= 0,V3 >= 0]). eq(start(V, V3, V4),0,[fun8(V, Out)],[V >= 0]). eq(start(V, V3, V4),0,[fun9(V, V3, Out)],[V >= 0,V3 >= 0]). eq(start(V, V3, V4),0,[fun10(V, Out)],[V >= 0]). eq(start(V, V3, V4),0,[fun11(V, Out)],[V >= 0]). eq(start(V, V3, V4),0,[fun12(V, V3, Out)],[V >= 0,V3 >= 0]). eq(start(V, V3, V4),0,[fun13(V, V3, Out)],[V >= 0,V3 >= 0]). eq(start(V, V3, V4),0,[fun14(V, V3, V4, Out)],[V >= 0,V3 >= 0,V4 >= 0]). eq(start(V, V3, V4),0,[fun15(V, V3, V4, Out)],[V >= 0,V3 >= 0,V4 >= 0]). eq(start(V, V3, V4),0,[fun16(V, V3, V4, Out)],[V >= 0,V3 >= 0,V4 >= 0]). eq(start(V, V3, V4),0,[fun17(V, V3, V4, Out)],[V >= 0,V3 >= 0,V4 >= 0]). eq(start(V, V3, V4),0,[isNat(V, Out)],[V >= 0]). eq(start(V, V3, V4),0,[isNatKind(V, Out)],[V >= 0]). eq(start(V, V3, V4),0,[fun18(Out)],[]). eq(start(V, V3, V4),0,[plus(V, V3, Out)],[V >= 0,V3 >= 0]). eq(start(V, V3, V4),0,[s(V, Out)],[V >= 0]). eq(start(V, V3, V4),0,[activate(V, Out)],[V >= 0]). eq(fun(V, V3, V4, Out),1,[activate(V11, Ret00),isNatKind(Ret00, Ret0),activate(V11, Ret1),activate(V21, Ret2),fun1(Ret0, Ret1, Ret2, Ret)],[Out = Ret,V11 >= 0,V21 >= 0,V = 0,V4 = V21,V3 = V11]). eq(fun1(V, V3, V4, Out),1,[activate(V22, Ret001),isNatKind(Ret001, Ret01),activate(V12, Ret11),activate(V22, Ret21),fun2(Ret01, Ret11, Ret21, Ret3)],[Out = Ret3,V12 >= 0,V22 >= 0,V = 0,V4 = V22,V3 = V12]). eq(fun2(V, V3, V4, Out),1,[activate(V23, Ret002),isNatKind(Ret002, Ret02),activate(V13, Ret12),activate(V23, Ret22),fun3(Ret02, Ret12, Ret22, Ret4)],[Out = Ret4,V13 >= 0,V23 >= 0,V = 0,V4 = V23,V3 = V13]). eq(fun3(V, V3, V4, Out),1,[activate(V14, Ret003),isNat(Ret003, Ret03),activate(V24, Ret13),fun4(Ret03, Ret13, Ret5)],[Out = Ret5,V14 >= 0,V24 >= 0,V = 0,V4 = V24,V3 = V14]). eq(fun4(V, V3, Out),1,[activate(V25, Ret004),isNat(Ret004, Ret04),fun5(Ret04, Ret6)],[Out = Ret6,V3 = V25,V25 >= 0,V = 0]). eq(fun5(V, Out),1,[],[Out = 0,V = 0]). eq(fun6(V, V3, Out),1,[activate(V15, Ret005),isNatKind(Ret005, Ret05),activate(V15, Ret14),fun7(Ret05, Ret14, Ret7)],[Out = Ret7,V15 >= 0,V = 0,V3 = V15]). eq(fun7(V, V3, Out),1,[activate(V16, Ret006),isNat(Ret006, Ret06),fun8(Ret06, Ret8)],[Out = Ret8,V16 >= 0,V = 0,V3 = V16]). eq(fun8(V, Out),1,[],[Out = 0,V = 0]). eq(fun9(V, V3, Out),1,[activate(V26, Ret007),isNatKind(Ret007, Ret07),fun10(Ret07, Ret9)],[Out = Ret9,V3 = V26,V26 >= 0,V = 0]). eq(fun10(V, Out),1,[],[Out = 0,V = 0]). eq(fun11(V, Out),1,[],[Out = 0,V = 0]). eq(fun12(V, V3, Out),1,[activate(N1, Ret008),isNatKind(Ret008, Ret08),activate(N1, Ret15),fun13(Ret08, Ret15, Ret10)],[Out = Ret10,V3 = N1,V = 0,N1 >= 0]). eq(fun13(V, V3, Out),1,[activate(N2, Ret16)],[Out = Ret16,V3 = N2,V = 0,N2 >= 0]). eq(fun14(V, V3, V4, Out),1,[activate(M1, Ret009),isNatKind(Ret009, Ret09),activate(M1, Ret17),activate(N3, Ret23),fun15(Ret09, Ret17, Ret23, Ret18)],[Out = Ret18,V3 = M1,V = 0,V4 = N3,M1 >= 0,N3 >= 0]). eq(fun15(V, V3, V4, Out),1,[activate(N4, Ret0010),isNat(Ret0010, Ret010),activate(M2, Ret19),activate(N4, Ret24),fun16(Ret010, Ret19, Ret24, Ret20)],[Out = Ret20,V3 = M2,V = 0,V4 = N4,M2 >= 0,N4 >= 0]). eq(fun16(V, V3, V4, Out),1,[activate(N5, Ret0011),isNatKind(Ret0011, Ret011),activate(M3, Ret110),activate(N5, Ret25),fun17(Ret011, Ret110, Ret25, Ret26)],[Out = Ret26,V3 = M3,V = 0,V4 = N5,M3 >= 0,N5 >= 0]). eq(fun17(V, V3, V4, Out),1,[activate(N6, Ret0012),activate(M4, Ret012),plus(Ret0012, Ret012, Ret013),s(Ret013, Ret27)],[Out = Ret27,V3 = M4,V = 0,V4 = N6,M4 >= 0,N6 >= 0]). eq(isNat(V, Out),1,[],[Out = 0,V = 0]). eq(isNat(V, Out),1,[activate(V17, Ret0013),isNatKind(Ret0013, Ret014),activate(V17, Ret111),activate(V27, Ret28),fun(Ret014, Ret111, Ret28, Ret29)],[Out = Ret29,V17 >= 0,V27 >= 0,V = 1 + V17 + V27]). eq(isNat(V, Out),1,[activate(V18, Ret0014),isNatKind(Ret0014, Ret015),activate(V18, Ret112),fun6(Ret015, Ret112, Ret30)],[Out = Ret30,V = 1 + V18,V18 >= 0]). eq(isNatKind(V, Out),1,[],[Out = 0,V = 0]). eq(isNatKind(V, Out),1,[activate(V19, Ret0015),isNatKind(Ret0015, Ret016),activate(V28, Ret113),fun9(Ret016, Ret113, Ret31)],[Out = Ret31,V19 >= 0,V28 >= 0,V = 1 + V19 + V28]). eq(isNatKind(V, Out),1,[activate(V110, Ret0016),isNatKind(Ret0016, Ret017),fun11(Ret017, Ret32)],[Out = Ret32,V = 1 + V110,V110 >= 0]). eq(fun18(Out),1,[],[Out = 0]). eq(plus(V, V3, Out),1,[],[Out = 1 + X11 + X21,X11 >= 0,X21 >= 0,V = X11,V3 = X21]). eq(s(V, Out),1,[],[Out = 1 + X3,X3 >= 0,V = X3]). eq(activate(V, Out),1,[fun18(Ret33)],[Out = Ret33,V = 0]). eq(activate(V, Out),1,[activate(X12, Ret018),activate(X22, Ret114),plus(Ret018, Ret114, Ret34)],[Out = Ret34,X12 >= 0,X22 >= 0,V = 1 + X12 + X22]). eq(activate(V, Out),1,[activate(X4, Ret019),s(Ret019, Ret35)],[Out = Ret35,V = 1 + X4,X4 >= 0]). eq(activate(V, Out),1,[],[Out = X5,X5 >= 0,V = X5]). input_output_vars(fun(V,V3,V4,Out),[V,V3,V4],[Out]). input_output_vars(fun1(V,V3,V4,Out),[V,V3,V4],[Out]). input_output_vars(fun2(V,V3,V4,Out),[V,V3,V4],[Out]). input_output_vars(fun3(V,V3,V4,Out),[V,V3,V4],[Out]). input_output_vars(fun4(V,V3,Out),[V,V3],[Out]). input_output_vars(fun5(V,Out),[V],[Out]). input_output_vars(fun6(V,V3,Out),[V,V3],[Out]). input_output_vars(fun7(V,V3,Out),[V,V3],[Out]). input_output_vars(fun8(V,Out),[V],[Out]). input_output_vars(fun9(V,V3,Out),[V,V3],[Out]). input_output_vars(fun10(V,Out),[V],[Out]). input_output_vars(fun11(V,Out),[V],[Out]). input_output_vars(fun12(V,V3,Out),[V,V3],[Out]). input_output_vars(fun13(V,V3,Out),[V,V3],[Out]). input_output_vars(fun14(V,V3,V4,Out),[V,V3,V4],[Out]). input_output_vars(fun15(V,V3,V4,Out),[V,V3,V4],[Out]). input_output_vars(fun16(V,V3,V4,Out),[V,V3,V4],[Out]). input_output_vars(fun17(V,V3,V4,Out),[V,V3,V4],[Out]). input_output_vars(isNat(V,Out),[V],[Out]). input_output_vars(isNatKind(V,Out),[V],[Out]). input_output_vars(fun18(Out),[],[Out]). input_output_vars(plus(V,V3,Out),[V,V3],[Out]). input_output_vars(s(V,Out),[V],[Out]). input_output_vars(activate(V,Out),[V],[Out]). |
CoFloCo proof output:
Preprocessing Cost Relations
=====================================
#### Computed strongly connected components
0. non_recursive : [fun18/1]
1. non_recursive : [plus/3]
2. non_recursive : [s/2]
3. recursive [non_tail,multiple] : [activate/2]
4. non_recursive : [fun5/2]
5. non_recursive : [fun8/2]
6. non_recursive : [fun11/2]
7. non_recursive : [fun10/2]
8. recursive [non_tail,multiple] : [fun9/3,isNatKind/2]
9. recursive [non_tail,multiple] : [fun/4,fun1/4,fun2/4,fun3/4,fun4/3,fun6/3,fun7/3,isNat/2]
10. non_recursive : [fun13/3]
11. non_recursive : [fun12/3]
12. non_recursive : [fun17/4]
13. non_recursive : [fun16/4]
14. non_recursive : [fun15/4]
15. non_recursive : [fun14/4]
16. non_recursive : [start/3]
#### Obtained direct recursion through partial evaluation
0. SCC is completely evaluated into other SCCs
1. SCC is completely evaluated into other SCCs
2. SCC is completely evaluated into other SCCs
3. SCC is partially evaluated into activate/2
4. SCC is completely evaluated into other SCCs
5. SCC is completely evaluated into other SCCs
6. SCC is completely evaluated into other SCCs
7. SCC is completely evaluated into other SCCs
8. SCC is partially evaluated into isNatKind/2
9. SCC is partially evaluated into isNat/2
10. SCC is completely evaluated into other SCCs
11. SCC is partially evaluated into fun12/3
12. SCC is partially evaluated into fun17/4
13. SCC is partially evaluated into fun16/4
14. SCC is partially evaluated into fun15/4
15. SCC is partially evaluated into fun14/4
16. SCC is partially evaluated into start/3
Control-Flow Refinement of Cost Relations
=====================================
### Specialization of cost equations activate/2
* CE 19 is refined into CE [34]
* CE 22 is refined into CE [35]
* CE 21 is refined into CE [36]
* CE 20 is refined into CE [37]
### Cost equations --> "Loop" of activate/2
* CEs [37] --> Loop 16
* CEs [36] --> Loop 17
* CEs [34,35] --> Loop 18
### Ranking functions of CR activate(V,Out)
* RF of phase [16,17]: [V]
#### Partial ranking functions of CR activate(V,Out)
* Partial RF of phase [16,17]:
- RF of loop [16:1,16:2,17:1]:
V
### Specialization of cost equations isNatKind/2
* CE 25 is refined into CE [38]
* CE 24 is refined into CE [39]
* CE 23 is refined into CE [40]
### Cost equations --> "Loop" of isNatKind/2
* CEs [40] --> Loop 19
* CEs [39] --> Loop 20
* CEs [38] --> Loop 21
### Ranking functions of CR isNatKind(V,Out)
* RF of phase [19,21]: [V]
#### Partial ranking functions of CR isNatKind(V,Out)
* Partial RF of phase [19,21]:
- RF of loop [19:1,19:2,21:1]:
V
### Specialization of cost equations isNat/2
* CE 28 is refined into CE [41]
* CE 27 is refined into CE [42,43,44,45]
* CE 26 is refined into CE [46,47]
### Cost equations --> "Loop" of isNat/2
* CEs [47] --> Loop 22
* CEs [46] --> Loop 23
* CEs [45] --> Loop 24
* CEs [44] --> Loop 25
* CEs [43] --> Loop 26
* CEs [42] --> Loop 27
* CEs [41] --> Loop 28
### Ranking functions of CR isNat(V,Out)
* RF of phase [22,24,25,26]: [V-1]
#### Partial ranking functions of CR isNat(V,Out)
* Partial RF of phase [22,24,25,26]:
- RF of loop [22:1,25:1,25:2,26:1,26:2]:
V-1
- RF of loop [24:1,24:2]:
V/2-1
### Specialization of cost equations fun12/3
* CE 29 is refined into CE [48,49]
### Cost equations --> "Loop" of fun12/3
* CEs [49] --> Loop 29
* CEs [48] --> Loop 30
### Ranking functions of CR fun12(V,V3,Out)
#### Partial ranking functions of CR fun12(V,V3,Out)
### Specialization of cost equations fun17/4
* CE 33 is refined into CE [50]
### Cost equations --> "Loop" of fun17/4
* CEs [50] --> Loop 31
### Ranking functions of CR fun17(V,V3,V4,Out)
#### Partial ranking functions of CR fun17(V,V3,V4,Out)
### Specialization of cost equations fun16/4
* CE 32 is refined into CE [51,52]
### Cost equations --> "Loop" of fun16/4
* CEs [52] --> Loop 32
* CEs [51] --> Loop 33
### Ranking functions of CR fun16(V,V3,V4,Out)
#### Partial ranking functions of CR fun16(V,V3,V4,Out)
### Specialization of cost equations fun15/4
* CE 31 is refined into CE [53,54,55]
### Cost equations --> "Loop" of fun15/4
* CEs [55] --> Loop 34
* CEs [54] --> Loop 35
* CEs [53] --> Loop 36
### Ranking functions of CR fun15(V,V3,V4,Out)
#### Partial ranking functions of CR fun15(V,V3,V4,Out)
### Specialization of cost equations fun14/4
* CE 30 is refined into CE [56,57,58,59,60,61]
### Cost equations --> "Loop" of fun14/4
* CEs [61] --> Loop 37
* CEs [60] --> Loop 38
* CEs [59] --> Loop 39
* CEs [58] --> Loop 40
* CEs [57] --> Loop 41
* CEs [56] --> Loop 42
### Ranking functions of CR fun14(V,V3,V4,Out)
#### Partial ranking functions of CR fun14(V,V3,V4,Out)
### Specialization of cost equations start/3
* CE 2 is refined into CE [62,63,64]
* CE 3 is refined into CE [65,66,67]
* CE 4 is refined into CE [68,69,70,71,72,73,74,75,76]
* CE 5 is refined into CE [77,78,79,80,81,82,83,84,85]
* CE 6 is refined into CE [86,87,88,89,90,91,92,93,94]
* CE 7 is refined into CE [95,96,97,98,99,100,101,102,103]
* CE 8 is refined into CE [104,105]
* CE 9 is refined into CE [106]
* CE 10 is refined into CE [107,108]
* CE 11 is refined into CE [109]
* CE 12 is refined into CE [110,111,112,113,114,115]
* CE 13 is refined into CE [116,117,118]
* CE 14 is refined into CE [119,120]
* CE 15 is refined into CE [121]
* CE 16 is refined into CE [122,123,124]
* CE 17 is refined into CE [125,126]
* CE 18 is refined into CE [127]
### Cost equations --> "Loop" of start/3
* CEs [62,63,64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101,102,103,104,105,106,107,108,109,110,111,112,113,114,115,116,117,118,119,120,121,122,123,124,125,126,127] --> Loop 43
### Ranking functions of CR start(V,V3,V4)
#### Partial ranking functions of CR start(V,V3,V4)
Computing Bounds
=====================================
#### Cost of chains of activate(V,Out):
* Chain [18]: 2
with precondition: [V=Out,V>=0]
* Chain [multiple([16,17],[[18]])]: 4*it(16)+2*it([18])+0
Such that:it([18]) =< V+1
aux(1) =< V
it(16) =< aux(1)
with precondition: [V=Out,V>=1]
#### Cost of chains of isNatKind(V,Out):
* Chain [20]: 1
with precondition: [V=0,Out=0]
* Chain [multiple([19,21],[[20]])]: 13*it(19)+1*it([20])+2*s(25)+4*s(26)+10*s(27)+8*s(28)+0
Such that:it([20]) =< V+1
aux(10) =< V
it(19) =< aux(10)
aux(6) =< aux(10)+1
aux(7) =< aux(10)
s(29) =< it(19)*aux(10)
s(31) =< it(19)*aux(6)
s(30) =< it(19)*aux(7)
s(25) =< it(19)*aux(6)
s(27) =< s(31)
s(28) =< s(30)
s(26) =< s(29)
with precondition: [Out=0,V>=1]
#### Cost of chains of isNat(V,Out):
* Chain [28]: 1
with precondition: [V=0,Out=0]
* Chain [multiple(27,[[28]])]: 30*s(35)+43
Such that:aux(12) =< 1
s(35) =< aux(12)
with precondition: [V=1,Out=0]
* Chain [23,28]: 10*s(80)+17
Such that:aux(14) =< 1
s(80) =< aux(14)
with precondition: [V=1,Out=0]
* Chain [multiple([22,24,25,26],[[28],[multiple(27,[[28]])],[23,28]])]: 14*it(22)+37*it(24)+78*it(25)+61*it([23,28])+12*s(431)+46*s(432)+4*s(433)+20*s(434)+16*s(435)+8*s(436)+88*s(442)+4*s(443)+20*s(444)+16*s(445)+8*s(446)+58*s(448)+4*s(449)+20*s(450)+16*s(451)+8*s(452)+34*s(462)+112*s(463)+8*s(464)+40*s(465)+32*s(466)+16*s(467)+30*s(468)+40*s(488)+0
Such that:aux(52) =< 1
aux(53) =< V
aux(54) =< V/2
aux(55) =< 2/3*V
it(22) =< aux(53)
it(24) =< aux(53)
it(25) =< aux(53)
it(24) =< aux(54)
it(25) =< aux(55)
aux(31) =< aux(53)+2
aux(30) =< aux(53)+1
aux(34) =< aux(53)
aux(46) =< it(25)+it(25)+it(24)+aux(52)
it([23,28]) =< it(25)+it(25)+it(24)+aux(52)
s(473) =< it(25)*aux(31)
s(472) =< it(25)*aux(30)
s(460) =< it(24)*aux(30)
s(459) =< it(24)*aux(34)
s(441) =< it(22)*aux(31)
s(440) =< it(22)*aux(30)
s(488) =< aux(46)
s(468) =< aux(55)
s(462) =< s(473)
s(463) =< s(472)
s(137) =< aux(30)+1
s(138) =< aux(30)
s(469) =< s(463)*aux(30)
s(471) =< s(463)*s(137)
s(470) =< s(463)*s(138)
s(464) =< s(463)*s(137)
s(465) =< s(471)
s(466) =< s(470)
s(467) =< s(469)
s(442) =< s(460)
s(448) =< s(459)
s(456) =< s(448)*aux(53)
s(458) =< s(448)*aux(30)
s(457) =< s(448)*aux(34)
s(449) =< s(448)*aux(30)
s(450) =< s(458)
s(451) =< s(457)
s(452) =< s(456)
s(453) =< s(442)*aux(30)
s(455) =< s(442)*s(137)
s(454) =< s(442)*s(138)
s(443) =< s(442)*s(137)
s(444) =< s(455)
s(445) =< s(454)
s(446) =< s(453)
s(431) =< s(441)
s(432) =< s(440)
s(437) =< s(432)*aux(30)
s(439) =< s(432)*s(137)
s(438) =< s(432)*s(138)
s(433) =< s(432)*s(137)
s(434) =< s(439)
s(435) =< s(438)
s(436) =< s(437)
with precondition: [Out=0,V>=2]
#### Cost of chains of fun12(V,V3,Out):
* Chain [30]: 6*s(497)+9
Such that:aux(58) =< 1
s(497) =< aux(58)
with precondition: [V=0,V3=0,Out=0]
* Chain [29]: 7*s(506)+25*s(507)+2*s(516)+10*s(517)+8*s(518)+4*s(519)+8
Such that:aux(59) =< V3
aux(60) =< V3+1
s(506) =< aux(60)
s(507) =< aux(59)
s(511) =< aux(59)+1
s(512) =< aux(59)
s(513) =< s(507)*aux(59)
s(514) =< s(507)*s(511)
s(515) =< s(507)*s(512)
s(516) =< s(507)*s(511)
s(517) =< s(514)
s(518) =< s(515)
s(519) =< s(513)
with precondition: [V=0,V3=Out,V3>=1]
#### Cost of chains of fun17(V,V3,V4,Out):
* Chain [31]: 2*s(527)+4*s(528)+2*s(530)+4*s(531)+7
Such that:s(529) =< V3
s(530) =< V3+1
s(526) =< V4
s(527) =< V4+1
s(531) =< s(529)
s(528) =< s(526)
with precondition: [V=0,V3+V4+2=Out,V3>=0,V4>=0]
#### Cost of chains of fun16(V,V3,V4,Out):
* Chain [33]: 6*s(533)+4*s(536)+8*s(537)+15
Such that:aux(62) =< 1
aux(63) =< V3
aux(64) =< V3+1
s(533) =< aux(62)
s(536) =< aux(64)
s(537) =< aux(63)
with precondition: [V=0,V4=0,V3+2=Out,V3>=0]
* Chain [32]: 7*s(548)+25*s(549)+2*s(558)+10*s(559)+8*s(560)+4*s(561)+4*s(563)+8*s(564)+14
Such that:aux(65) =< V3
aux(66) =< V3+1
aux(67) =< V4
aux(68) =< V4+1
s(563) =< aux(66)
s(548) =< aux(68)
s(564) =< aux(65)
s(549) =< aux(67)
s(553) =< aux(67)+1
s(554) =< aux(67)
s(555) =< s(549)*aux(67)
s(556) =< s(549)*s(553)
s(557) =< s(549)*s(554)
s(558) =< s(549)*s(553)
s(559) =< s(556)
s(560) =< s(557)
s(561) =< s(555)
with precondition: [V=0,V3+V4+2=Out,V3>=0,V4>=1]
#### Cost of chains of fun15(V,V3,V4,Out):
* Chain [36]: 10*s(575)+6*s(578)+12*s(579)+23
Such that:aux(70) =< 1
aux(71) =< V3
aux(72) =< V3+1
s(575) =< aux(70)
s(578) =< aux(72)
s(579) =< aux(71)
with precondition: [V=0,V4=0,V3+2=Out,V3>=0]
* Chain [35]: 11*s(590)+33*s(591)+6*s(593)+12*s(594)+2*s(611)+10*s(612)+8*s(613)+4*s(614)+104
Such that:aux(73) =< 1
aux(74) =< 2
aux(75) =< V3
aux(76) =< V3+1
s(590) =< aux(74)
s(593) =< aux(76)
s(594) =< aux(75)
s(591) =< aux(73)
s(606) =< aux(73)+1
s(607) =< aux(73)
s(608) =< s(591)*aux(73)
s(609) =< s(591)*s(606)
s(610) =< s(591)*s(607)
s(611) =< s(591)*s(606)
s(612) =< s(609)
s(613) =< s(610)
s(614) =< s(608)
with precondition: [V=0,V4=1,V3+3=Out,V3>=0]
* Chain [34]: 11*s(616)+47*s(617)+37*s(623)+78*s(624)+61*s(629)+40*s(636)+30*s(637)+34*s(638)+112*s(639)+8*s(645)+40*s(646)+32*s(647)+16*s(648)+88*s(649)+58*s(650)+4*s(654)+20*s(655)+16*s(656)+8*s(657)+4*s(661)+20*s(662)+16*s(663)+8*s(664)+12*s(665)+56*s(666)+4*s(670)+20*s(671)+16*s(672)+8*s(673)+6*s(675)+12*s(676)+2*s(693)+8*s(695)+4*s(696)+21
Such that:s(618) =< 1
s(620) =< V4/2
s(621) =< 2/3*V4
aux(77) =< V3
aux(78) =< V3+1
aux(79) =< V4
aux(80) =< V4+1
s(675) =< aux(78)
s(616) =< aux(80)
s(676) =< aux(77)
s(617) =< aux(79)
s(626) =< aux(79)+1
s(627) =< aux(79)
s(690) =< s(617)*aux(79)
s(635) =< s(617)*s(626)
s(692) =< s(617)*s(627)
s(693) =< s(617)*s(626)
s(666) =< s(635)
s(695) =< s(692)
s(696) =< s(690)
s(623) =< aux(79)
s(624) =< aux(79)
s(623) =< s(620)
s(624) =< s(621)
s(625) =< aux(79)+2
s(628) =< s(624)+s(624)+s(623)+s(618)
s(629) =< s(624)+s(624)+s(623)+s(618)
s(630) =< s(624)*s(625)
s(631) =< s(624)*s(626)
s(632) =< s(623)*s(626)
s(633) =< s(623)*s(627)
s(634) =< s(617)*s(625)
s(636) =< s(628)
s(637) =< s(621)
s(638) =< s(630)
s(639) =< s(631)
s(640) =< s(626)+1
s(641) =< s(626)
s(642) =< s(639)*s(626)
s(643) =< s(639)*s(640)
s(644) =< s(639)*s(641)
s(645) =< s(639)*s(640)
s(646) =< s(643)
s(647) =< s(644)
s(648) =< s(642)
s(649) =< s(632)
s(650) =< s(633)
s(651) =< s(650)*aux(79)
s(652) =< s(650)*s(626)
s(653) =< s(650)*s(627)
s(654) =< s(650)*s(626)
s(655) =< s(652)
s(656) =< s(653)
s(657) =< s(651)
s(658) =< s(649)*s(626)
s(659) =< s(649)*s(640)
s(660) =< s(649)*s(641)
s(661) =< s(649)*s(640)
s(662) =< s(659)
s(663) =< s(660)
s(664) =< s(658)
s(665) =< s(634)
s(667) =< s(666)*s(626)
s(668) =< s(666)*s(640)
s(669) =< s(666)*s(641)
s(670) =< s(666)*s(640)
s(671) =< s(668)
s(672) =< s(669)
s(673) =< s(667)
with precondition: [V=0,V3+V4+2=Out,V3>=0,V4>=2]
#### Cost of chains of fun14(V,V3,V4,Out):
* Chain [42]: 22*s(698)+31
Such that:aux(82) =< 1
s(698) =< aux(82)
with precondition: [V=0,V3=0,V4=0,Out=2]
* Chain [41]: 47*s(713)+13*s(719)+2*s(734)+10*s(735)+8*s(736)+4*s(737)+112
Such that:aux(84) =< 1
aux(85) =< 2
s(713) =< aux(84)
s(719) =< aux(85)
s(729) =< aux(84)+1
s(730) =< aux(84)
s(731) =< s(713)*aux(84)
s(732) =< s(713)*s(729)
s(733) =< s(713)*s(730)
s(734) =< s(713)*s(729)
s(735) =< s(732)
s(736) =< s(733)
s(737) =< s(731)
with precondition: [V=0,V3=0,V4=1,Out=3]
* Chain [40]: 10*s(739)+13*s(745)+51*s(746)+2*s(763)+56*s(764)+8*s(765)+4*s(766)+37*s(767)+78*s(768)+61*s(771)+40*s(777)+30*s(778)+34*s(779)+112*s(780)+8*s(786)+40*s(787)+32*s(788)+16*s(789)+88*s(790)+58*s(791)+4*s(795)+20*s(796)+16*s(797)+8*s(798)+4*s(802)+20*s(803)+16*s(804)+8*s(805)+12*s(806)+4*s(810)+20*s(811)+16*s(812)+8*s(813)+29
Such that:s(748) =< V4/2
s(749) =< 2/3*V4
aux(87) =< 1
aux(88) =< V4
aux(89) =< V4+1
s(739) =< aux(87)
s(745) =< aux(89)
s(746) =< aux(88)
s(758) =< aux(88)+1
s(759) =< aux(88)
s(760) =< s(746)*aux(88)
s(761) =< s(746)*s(758)
s(762) =< s(746)*s(759)
s(763) =< s(746)*s(758)
s(764) =< s(761)
s(765) =< s(762)
s(766) =< s(760)
s(767) =< aux(88)
s(768) =< aux(88)
s(767) =< s(748)
s(768) =< s(749)
s(769) =< aux(88)+2
s(770) =< s(768)+s(768)+s(767)+aux(87)
s(771) =< s(768)+s(768)+s(767)+aux(87)
s(772) =< s(768)*s(769)
s(773) =< s(768)*s(758)
s(774) =< s(767)*s(758)
s(775) =< s(767)*s(759)
s(776) =< s(746)*s(769)
s(777) =< s(770)
s(778) =< s(749)
s(779) =< s(772)
s(780) =< s(773)
s(781) =< s(758)+1
s(782) =< s(758)
s(783) =< s(780)*s(758)
s(784) =< s(780)*s(781)
s(785) =< s(780)*s(782)
s(786) =< s(780)*s(781)
s(787) =< s(784)
s(788) =< s(785)
s(789) =< s(783)
s(790) =< s(774)
s(791) =< s(775)
s(792) =< s(791)*aux(88)
s(793) =< s(791)*s(758)
s(794) =< s(791)*s(759)
s(795) =< s(791)*s(758)
s(796) =< s(793)
s(797) =< s(794)
s(798) =< s(792)
s(799) =< s(790)*s(758)
s(800) =< s(790)*s(781)
s(801) =< s(790)*s(782)
s(802) =< s(790)*s(781)
s(803) =< s(800)
s(804) =< s(801)
s(805) =< s(799)
s(806) =< s(776)
s(807) =< s(764)*s(758)
s(808) =< s(764)*s(781)
s(809) =< s(764)*s(782)
s(810) =< s(764)*s(781)
s(811) =< s(808)
s(812) =< s(809)
s(813) =< s(807)
with precondition: [V=0,V3=0,V4+2=Out,V4>=2]
* Chain [39]: 11*s(815)+33*s(816)+2*s(825)+10*s(826)+8*s(827)+4*s(828)+12*s(833)+30
Such that:aux(90) =< 1
aux(91) =< V3
aux(92) =< V3+1
s(833) =< aux(90)
s(815) =< aux(92)
s(816) =< aux(91)
s(820) =< aux(91)+1
s(821) =< aux(91)
s(822) =< s(816)*aux(91)
s(823) =< s(816)*s(820)
s(824) =< s(816)*s(821)
s(825) =< s(816)*s(820)
s(826) =< s(823)
s(827) =< s(824)
s(828) =< s(822)
with precondition: [V=0,V4=0,V3+2=Out,V3>=1]
* Chain [38]: 11*s(842)+33*s(843)+2*s(852)+10*s(853)+8*s(854)+4*s(855)+13*s(860)+37*s(861)+2*s(875)+10*s(876)+8*s(877)+4*s(878)+111
Such that:aux(93) =< 1
aux(94) =< 2
aux(95) =< V3
aux(96) =< V3+1
s(860) =< aux(94)
s(842) =< aux(96)
s(843) =< aux(95)
s(861) =< aux(93)
s(870) =< aux(93)+1
s(871) =< aux(93)
s(872) =< s(861)*aux(93)
s(873) =< s(861)*s(870)
s(874) =< s(861)*s(871)
s(875) =< s(861)*s(870)
s(876) =< s(873)
s(877) =< s(874)
s(878) =< s(872)
s(847) =< aux(95)+1
s(848) =< aux(95)
s(849) =< s(843)*aux(95)
s(850) =< s(843)*s(847)
s(851) =< s(843)*s(848)
s(852) =< s(843)*s(847)
s(853) =< s(850)
s(854) =< s(851)
s(855) =< s(849)
with precondition: [V=0,V4=1,V3+3=Out,V3>=1]
* Chain [37]: 11*s(880)+33*s(881)+2*s(890)+10*s(891)+8*s(892)+4*s(893)+13*s(898)+51*s(899)+2*s(916)+56*s(917)+8*s(918)+4*s(919)+37*s(920)+78*s(921)+61*s(924)+40*s(930)+30*s(931)+34*s(932)+112*s(933)+8*s(939)+40*s(940)+32*s(941)+16*s(942)+88*s(943)+58*s(944)+4*s(948)+20*s(949)+16*s(950)+8*s(951)+4*s(955)+20*s(956)+16*s(957)+8*s(958)+12*s(959)+4*s(963)+20*s(964)+16*s(965)+8*s(966)+28
Such that:s(900) =< 1
s(901) =< V4/2
s(902) =< 2/3*V4
aux(97) =< V3
aux(98) =< V3+1
aux(99) =< V4
aux(100) =< V4+1
s(880) =< aux(98)
s(898) =< aux(100)
s(881) =< aux(97)
s(899) =< aux(99)
s(911) =< aux(99)+1
s(912) =< aux(99)
s(913) =< s(899)*aux(99)
s(914) =< s(899)*s(911)
s(915) =< s(899)*s(912)
s(916) =< s(899)*s(911)
s(917) =< s(914)
s(918) =< s(915)
s(919) =< s(913)
s(920) =< aux(99)
s(921) =< aux(99)
s(920) =< s(901)
s(921) =< s(902)
s(922) =< aux(99)+2
s(923) =< s(921)+s(921)+s(920)+s(900)
s(924) =< s(921)+s(921)+s(920)+s(900)
s(925) =< s(921)*s(922)
s(926) =< s(921)*s(911)
s(927) =< s(920)*s(911)
s(928) =< s(920)*s(912)
s(929) =< s(899)*s(922)
s(930) =< s(923)
s(931) =< s(902)
s(932) =< s(925)
s(933) =< s(926)
s(934) =< s(911)+1
s(935) =< s(911)
s(936) =< s(933)*s(911)
s(937) =< s(933)*s(934)
s(938) =< s(933)*s(935)
s(939) =< s(933)*s(934)
s(940) =< s(937)
s(941) =< s(938)
s(942) =< s(936)
s(943) =< s(927)
s(944) =< s(928)
s(945) =< s(944)*aux(99)
s(946) =< s(944)*s(911)
s(947) =< s(944)*s(912)
s(948) =< s(944)*s(911)
s(949) =< s(946)
s(950) =< s(947)
s(951) =< s(945)
s(952) =< s(943)*s(911)
s(953) =< s(943)*s(934)
s(954) =< s(943)*s(935)
s(955) =< s(943)*s(934)
s(956) =< s(953)
s(957) =< s(954)
s(958) =< s(952)
s(959) =< s(929)
s(960) =< s(917)*s(911)
s(961) =< s(917)*s(934)
s(962) =< s(917)*s(935)
s(963) =< s(917)*s(934)
s(964) =< s(961)
s(965) =< s(962)
s(966) =< s(960)
s(885) =< aux(97)+1
s(886) =< aux(97)
s(887) =< s(881)*aux(97)
s(888) =< s(881)*s(885)
s(889) =< s(881)*s(886)
s(890) =< s(881)*s(885)
s(891) =< s(888)
s(892) =< s(889)
s(893) =< s(887)
with precondition: [V=0,V3+V4+2=Out,V3>=1,V4>=2]
#### Cost of chains of start(V,V3,V4):
* Chain [43]: 996*s(968)+244*s(977)+44*s(987)+220*s(988)+176*s(989)+88*s(990)+151*s(998)+597*s(999)+18*s(1008)+734*s(1009)+72*s(1010)+36*s(1011)+518*s(1023)+1092*s(1024)+854*s(1029)+560*s(1036)+420*s(1037)+476*s(1038)+1568*s(1039)+112*s(1045)+560*s(1046)+448*s(1047)+224*s(1048)+1232*s(1049)+812*s(1050)+56*s(1054)+280*s(1055)+224*s(1056)+112*s(1057)+56*s(1061)+280*s(1062)+224*s(1063)+112*s(1064)+168*s(1065)+56*s(1070)+280*s(1071)+224*s(1072)+112*s(1073)+175*s(1242)+769*s(1243)+38*s(1255)+880*s(1256)+152*s(1257)+76*s(1258)+555*s(1300)+1170*s(1301)+915*s(1306)+600*s(1313)+450*s(1314)+510*s(1315)+1680*s(1316)+120*s(1322)+600*s(1323)+480*s(1324)+240*s(1325)+1320*s(1326)+870*s(1327)+60*s(1331)+300*s(1332)+240*s(1333)+120*s(1334)+60*s(1338)+300*s(1339)+240*s(1340)+120*s(1341)+180*s(1342)+60*s(1347)+300*s(1348)+240*s(1349)+120*s(1350)+31*s(4080)+37*s(4081)+78*s(4082)+61*s(4087)+40*s(4094)+30*s(4095)+34*s(4096)+112*s(4097)+8*s(4103)+40*s(4104)+32*s(4105)+16*s(4106)+88*s(4107)+58*s(4108)+4*s(4112)+20*s(4113)+16*s(4114)+8*s(4115)+4*s(4119)+20*s(4120)+16*s(4121)+8*s(4122)+12*s(4123)+56*s(4124)+4*s(4128)+20*s(4129)+16*s(4130)+8*s(4131)+3*s(4132)+2*s(4140)+8*s(4142)+4*s(4143)+196
Such that:s(4078) =< V/2
s(4079) =< 2/3*V
aux(227) =< 1
aux(228) =< 2
aux(229) =< V
aux(230) =< V+1
aux(231) =< V3
aux(232) =< V3+1
aux(233) =< V3/2
aux(234) =< 2/3*V3
aux(235) =< V4
aux(236) =< V4+1
aux(237) =< V4/2
aux(238) =< 2/3*V4
s(968) =< aux(227)
s(977) =< aux(228)
s(4132) =< aux(230)
s(998) =< aux(232)
s(1242) =< aux(236)
s(982) =< aux(227)+1
s(983) =< aux(227)
s(984) =< s(968)*aux(227)
s(985) =< s(968)*s(982)
s(986) =< s(968)*s(983)
s(987) =< s(968)*s(982)
s(988) =< s(985)
s(989) =< s(986)
s(990) =< s(984)
s(999) =< aux(231)
s(1023) =< aux(231)
s(1024) =< aux(231)
s(1023) =< aux(233)
s(1024) =< aux(234)
s(1025) =< aux(231)+2
s(1003) =< aux(231)+1
s(1004) =< aux(231)
s(1028) =< s(1024)+s(1024)+s(1023)+aux(227)
s(1029) =< s(1024)+s(1024)+s(1023)+aux(227)
s(1030) =< s(1024)*s(1025)
s(1031) =< s(1024)*s(1003)
s(1032) =< s(1023)*s(1003)
s(1033) =< s(1023)*s(1004)
s(1034) =< s(999)*s(1025)
s(1006) =< s(999)*s(1003)
s(1036) =< s(1028)
s(1037) =< aux(234)
s(1038) =< s(1030)
s(1039) =< s(1031)
s(1040) =< s(1003)+1
s(1041) =< s(1003)
s(1042) =< s(1039)*s(1003)
s(1043) =< s(1039)*s(1040)
s(1044) =< s(1039)*s(1041)
s(1045) =< s(1039)*s(1040)
s(1046) =< s(1043)
s(1047) =< s(1044)
s(1048) =< s(1042)
s(1049) =< s(1032)
s(1050) =< s(1033)
s(1051) =< s(1050)*aux(231)
s(1052) =< s(1050)*s(1003)
s(1053) =< s(1050)*s(1004)
s(1054) =< s(1050)*s(1003)
s(1055) =< s(1052)
s(1056) =< s(1053)
s(1057) =< s(1051)
s(1058) =< s(1049)*s(1003)
s(1059) =< s(1049)*s(1040)
s(1060) =< s(1049)*s(1041)
s(1061) =< s(1049)*s(1040)
s(1062) =< s(1059)
s(1063) =< s(1060)
s(1064) =< s(1058)
s(1065) =< s(1034)
s(1009) =< s(1006)
s(1067) =< s(1009)*s(1003)
s(1068) =< s(1009)*s(1040)
s(1069) =< s(1009)*s(1041)
s(1070) =< s(1009)*s(1040)
s(1071) =< s(1068)
s(1072) =< s(1069)
s(1073) =< s(1067)
s(1005) =< s(999)*aux(231)
s(1007) =< s(999)*s(1004)
s(1008) =< s(999)*s(1003)
s(1010) =< s(1007)
s(1011) =< s(1005)
s(1243) =< aux(235)
s(1250) =< aux(235)+1
s(1251) =< aux(235)
s(1252) =< s(1243)*aux(235)
s(1253) =< s(1243)*s(1250)
s(1254) =< s(1243)*s(1251)
s(1255) =< s(1243)*s(1250)
s(1256) =< s(1253)
s(1257) =< s(1254)
s(1258) =< s(1252)
s(1300) =< aux(235)
s(1301) =< aux(235)
s(1300) =< aux(237)
s(1301) =< aux(238)
s(1302) =< aux(235)+2
s(1305) =< s(1301)+s(1301)+s(1300)+aux(227)
s(1306) =< s(1301)+s(1301)+s(1300)+aux(227)
s(1307) =< s(1301)*s(1302)
s(1308) =< s(1301)*s(1250)
s(1309) =< s(1300)*s(1250)
s(1310) =< s(1300)*s(1251)
s(1311) =< s(1243)*s(1302)
s(1313) =< s(1305)
s(1314) =< aux(238)
s(1315) =< s(1307)
s(1316) =< s(1308)
s(1317) =< s(1250)+1
s(1318) =< s(1250)
s(1319) =< s(1316)*s(1250)
s(1320) =< s(1316)*s(1317)
s(1321) =< s(1316)*s(1318)
s(1322) =< s(1316)*s(1317)
s(1323) =< s(1320)
s(1324) =< s(1321)
s(1325) =< s(1319)
s(1326) =< s(1309)
s(1327) =< s(1310)
s(1328) =< s(1327)*aux(235)
s(1329) =< s(1327)*s(1250)
s(1330) =< s(1327)*s(1251)
s(1331) =< s(1327)*s(1250)
s(1332) =< s(1329)
s(1333) =< s(1330)
s(1334) =< s(1328)
s(1335) =< s(1326)*s(1250)
s(1336) =< s(1326)*s(1317)
s(1337) =< s(1326)*s(1318)
s(1338) =< s(1326)*s(1317)
s(1339) =< s(1336)
s(1340) =< s(1337)
s(1341) =< s(1335)
s(1342) =< s(1311)
s(1344) =< s(1256)*s(1250)
s(1345) =< s(1256)*s(1317)
s(1346) =< s(1256)*s(1318)
s(1347) =< s(1256)*s(1317)
s(1348) =< s(1345)
s(1349) =< s(1346)
s(1350) =< s(1344)
s(4080) =< aux(229)
s(4081) =< aux(229)
s(4082) =< aux(229)
s(4081) =< s(4078)
s(4082) =< s(4079)
s(4083) =< aux(229)+2
s(4084) =< aux(229)+1
s(4085) =< aux(229)
s(4086) =< s(4082)+s(4082)+s(4081)+aux(227)
s(4087) =< s(4082)+s(4082)+s(4081)+aux(227)
s(4088) =< s(4082)*s(4083)
s(4089) =< s(4082)*s(4084)
s(4090) =< s(4081)*s(4084)
s(4091) =< s(4081)*s(4085)
s(4092) =< s(4080)*s(4083)
s(4093) =< s(4080)*s(4084)
s(4094) =< s(4086)
s(4095) =< s(4079)
s(4096) =< s(4088)
s(4097) =< s(4089)
s(4098) =< s(4084)+1
s(4099) =< s(4084)
s(4100) =< s(4097)*s(4084)
s(4101) =< s(4097)*s(4098)
s(4102) =< s(4097)*s(4099)
s(4103) =< s(4097)*s(4098)
s(4104) =< s(4101)
s(4105) =< s(4102)
s(4106) =< s(4100)
s(4107) =< s(4090)
s(4108) =< s(4091)
s(4109) =< s(4108)*aux(229)
s(4110) =< s(4108)*s(4084)
s(4111) =< s(4108)*s(4085)
s(4112) =< s(4108)*s(4084)
s(4113) =< s(4110)
s(4114) =< s(4111)
s(4115) =< s(4109)
s(4116) =< s(4107)*s(4084)
s(4117) =< s(4107)*s(4098)
s(4118) =< s(4107)*s(4099)
s(4119) =< s(4107)*s(4098)
s(4120) =< s(4117)
s(4121) =< s(4118)
s(4122) =< s(4116)
s(4123) =< s(4092)
s(4124) =< s(4093)
s(4125) =< s(4124)*s(4084)
s(4126) =< s(4124)*s(4098)
s(4127) =< s(4124)*s(4099)
s(4128) =< s(4124)*s(4098)
s(4129) =< s(4126)
s(4130) =< s(4127)
s(4131) =< s(4125)
s(4137) =< s(4080)*aux(229)
s(4139) =< s(4080)*s(4085)
s(4140) =< s(4080)*s(4084)
s(4142) =< s(4139)
s(4143) =< s(4137)
with precondition: []
Closed-form bounds of start(V,V3,V4):
-------------------------------------
* Chain [43] with precondition: []
- Upper bound: nat(V)*1087+5502+nat(V)*878*nat(V)+nat(V)*240*nat(V)*nat(V)+nat(V3)*15321+nat(V3)*12172*nat(V3)+nat(V3)*3360*nat(V3)*nat(V3)+nat(V4)*16657+nat(V4)*13266*nat(V4)+nat(V4)*3600*nat(V4)*nat(V4)+nat(2/3*V)*30+nat(2/3*V3)*420+nat(2/3*V4)*450+nat(V+1)*3+nat(V3+1)*151+nat(V4+1)*175
- Complexity: n^3
### Maximum cost of start(V,V3,V4): nat(V)*1087+5502+nat(V)*878*nat(V)+nat(V)*240*nat(V)*nat(V)+nat(V3)*15321+nat(V3)*12172*nat(V3)+nat(V3)*3360*nat(V3)*nat(V3)+nat(V4)*16657+nat(V4)*13266*nat(V4)+nat(V4)*3600*nat(V4)*nat(V4)+nat(2/3*V)*30+nat(2/3*V3)*420+nat(2/3*V4)*450+nat(V+1)*3+nat(V3+1)*151+nat(V4+1)*175
Asymptotic class: n^3
* Total analysis performed in 14765 ms.